COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	verifiability and reliability of software
C00004 00003	hoare
C00005 ENDMK
C⊗;
verifiability and reliability of software

the problem

what is programming
composition and specification
modification-editing
debugging tracing and breaking
verifying
compiling
running

first 5 involve using d.s. rep of prog.

on spec lang: is it efficient
1. does it waste my time

2. efficient use of storage structures.


what to do
 professionalism
 theory
 teaching w.o. research in c.s. loses.

reliability ≠ correctness
 protection
 compare operating system, which has been proved correct and
 user programs, proved corect therefore running w.o. protection.
 its just asking for trouble.

history of results

programming lab


hoare
scott
 wadsworth and co
a.d.s.
modularity
  clu
correctness of translators
on-line etv, raid